Nuprl Lemma : bool-to-neg-dcdr_wf
11,40
postcript
pdf
A
:Type,
f
:(
A
),
x
:
A
. {
f
}
(
x
)
Dec(
f
(
x
) = ff)
latex
ProofTree
Definitions
x
:
A
.
B
(
x
)
,
Dec(
P
)
,
s
=
t
,
f
(
a
)
,
{
f
}
,
x
:
A
B
(
x
)
,
,
t
T
,
Type
,
ff
,
bool-to-neg-dcdr-aux
,
Lemmas
bfalse
wf
,
decidable
wf
,
bool-to-neg-dcdr-aux
,
bool
wf
origin
A:Type, f:(A
), x:A. {f}
(x) 
Dec(f(x) = ff)
A:Type, f:(A), x:A. {f}(x) Dec(f(x) = ff)
x:A. B(x)B(x) T